perm filename ONE.PRF[226,JMC] blob
sn#005411 filedate 1972-07-26 generic text, type T, neo UTF8
AXIOM SCW1
(∀ W) (SCWORLD W⊃ISSETSET BASIS W∧(∀ U) (UεBASIS W⊃¬ (UUεU)))
AXIOM SCW2
(∀ W) (SCWORLD W⊃(∀ U) (UεBASIS W⊃TORD UεORDERINGS W))
AXIOM SCW3
(∀ W) (SCWORLD W∧R1εORDERINGS W∧R2εORDERINGS W⊃R1→→R2εORDERINGS W)
AXIOM SCW4
(∀ W) (∀ Z) (SCWORLD W∧(∀ U) (UεBASIS W⊃TORD UεZ)∧(∀ R1) (∀ R2) (R1ε
Z∧R2εZ⊃R1→→R2εZ)⊃ORDERINGS W⊂Z)
AXIOM SCW5
(∀ W) (∀ S) (∀ V) (∀ R) (SCWORLD W∧SεSTATES W∧RεORDERINGS W∧VεTERMS
(R,W)⊃C(V,S)εDOMAIN R)
AXIOM SCW6
(∀ W) (SCWORLD W⊃STATES W≠NULLSET)
AXIOM SCW7
(∀ W) (∀ R) (SCWORLD W∧RεORDERINGS W⊃INFINITE VARS R∧VARS R⊂TERMS(R
,W))
AXIOM SCW8
(∀ W) (∀ R) (∀ X) (SCWORLD W∧RεORDERINGS W∧XεDOMAIN R⊃MKCONST Xε
TERMS(R,W)∧ISCONST MKCONST X∧VALUE MKCONST X=X∧(∀ S) (SεSTATES W⊃C(
MKCONST X,S)=X))
AXIOM SCW9
(∀ W) (∀ R) (∀ V) (∀ X) (∀ S) (SCWORLD W∧RεORDERINGS W∧VεVARS R∧Xε
DOMAIN R∧SεSTATES W⊃A(V,X,S)εSTATES W∧C(V,A(V,X,S))=X∧(∀ R1) (∀ V1)
(R1εORDERINGS W∧V1εVARS R∧V1≠V⊃C(V1,A(V,X,S))=C(V1,S)))
AXIOM SCW10
(∀ W) (∀ R) (∀ V) (SCWORLD W∧RεORDERINGS W∧VεVARS R⊃FREEVARS V=
UNITSET V)
AXIOM SCW11
(∀ W) (∀ R) (∀ E) (SCWORLD W∧RεORDERINGS W∧EεTERMS(R,W)∧ISCONST E⊃
FREEVARS E=NULLSET)
AXIOM SCW12
(∀ W) (∀ R1) (∀ E1) (∀ R2) (∀ E) (∀ S) (SCWORLD W∧R1εORDERINGS W∧E1ε
TERMS(R1,W)∧R2εORDERINGS W∧EεTERMS(R1→→R2,W)∧SεSTATES W⊃α(E,E1)ε
TERMS(R2,W)∧FREEVARS α(E,E1)=FREEVARS E∪FREEVARS E1∧C(α(E,E1),S)=β(C
(E,S),C(E1,S)))
AXIOM SCW13
(∀ W) (∀ R1) (∀ R2) (∀ V1) (∀ E2) (∀ S) (SCWORLD W∧R1εORDERINGS W∧R2
εORDERINGS W∧V1εVARS R1∧V2εTERMS(R2,W)∧SεSTATES W⊃LAM(V1,E2)εTERMS(
R1→→R2,W)∧FREEVARS LAM(V1,E2)=FREEVARS E2-UNITSET V1∧(∀ X) (XεDOMAIN
R1⊃β(C(LAM(V1,E2),S),X)=C(E2,A(V1,X,S))))
AXIOM SCW14
(∀ W) (∀ R) (∀ F) (∀ V) (∀ S) (SCWORLD W∧RεORDERINGS W∧FεTERMS(R→→R
,W)∧VεVARS R∧SεSTATES W⊃MU(V,F)εTERMS(R,W)∧FREEVARS MU(V,F)=FREEVARS
F-UNITSET V∧C(MU(V,F),S)=β(C(F,S),C(MU(V,F),S))∧(∀ X) (XεDOM R∧C(X
,S)=β(C(F,S),C(X,S))⊃ββ(C(MU(V,F),S),R,X)))
AXIOM SCW15
(∀ W) (∀ E1) (∀ E2) (∀ R) (SCWORLD W∧RεORDERINGS W∧E1εTERMS(R,W)∧E2ε
TERMS W∧(∀ S) (SεSTATES W⊃C(E1,S)=C(E2,S))⊃E1=E2)
AXIOM SCW16
(∀ W) (∀ R) (∀ P) (∀ E1) (∀ E2) (SCWORLD W∧RεORDERINGS W∧PεTERMS(
TORD TV,W)∧E1εTERMS(R,W)∧E2εTERMS(R,W)⊃IFF(P,E1,E2)εTERMS(R,W)∧(∀ S
) (SεSTATES W⊃C(IFF(P,E1,E2),S)=IF C(P,S)=TRUE THEN C(E1,S) ELSE C(
E2,S)))
AXIOM SCW17
(∀ W) (∀ R) (∀ E) (∀ S1) (∀ S2) (SCWORLD W∧RεORDERINGS W∧EεTERMS(R,W
)∧S1εSTATES W∧S2εSTATES W∧(∀ V) (VεFREEVARS E C(V,S1)=C(V,S2))⊃C(E,
S1)=C(E,S2))
AXIOM SCW18
(∀ W) (∀ R) (SCWORLD W∧RεORDERINGS W⊃INFINITE VARS(R,W))
AXIOM ISSET
(∀ X) (∀ Y) (XεY⊃ISSET Y)
AXIOM EXTENSIONALITY
(∀ U) (∀ V) (ISSET U∧ISSET V⊃(∀ X) (XεU≡XεV)⊃U=V)
AXIOM NULLSET
ISSET NULLSET
AXIOM NULL1
(∀ X) ¬ (XεNULLSET)
AXIOM UNITSET
(∀ X) (∀ Y) (YεUNITSET X≡Y=X)
AXIOM UNIONSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X∪Y))
AXIOM UNIONAX
(∀ X) (∀ Y) (∀ Z) (ZεX∪Y≡ZεX∨ZεY)
AXIOM INTERSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X∩Y))
AXIOM INTER
(∀ X) (∀ Y) (∀ Z) (ZεX∩Y≡ZεX∨ZεY)
AXIOM CARTSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X⊗Y))
AXIOM CARTESIAN
(∀ X) (∀ Y) (∀ Z) (ZεX⊗Y≡(∃ U) (∃ V) (UεX∧VεY∧Z=U.V))
AXIOM PAIR
(∀ X) (∀ Y) (∀ U) (∀ V) (X.Y=U.V≡X=U∧Y=V)
AXIOM CONTAIN
(∀ U) (∀ V) (U⊂V≡(∀ X) (XεU⊃XεV))
AXIOM POWERSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X→Y)∧(∀ F) (FεX→Y⊃ISMAP F∧X=
DOMAIN F∧Y=RANGE F))
AXIOM MAP
(∀ F) (ISMAP F⊃ISSET DOMAIN F∧ISSET RANGE F FεDOMAIN F→RANGE F)
AXIOM APPLY
(∀ F) (∀ X) (∀ U) (∀ V) (FεU→V∧XεU⊃β(F,X)εV)
AXIOM FEXTENSIONALITY
(∀ U) (∀ V) (∀ F) (∀ G) (FεU→V∧GεU→V⊃(F=G≡(∀ X) (XεU⊃β(F,X)=β(G,X))
))
AXIOM FNDEF
(∀ FF) (∀ U) (∀ V) (ISSET U∧ISSET V∧ISSET FF∧FF⊂U⊗V∧(∀ X) (XεU⊃(∃ Y
) (YεV∧X.YεFF))∧(∀ X) (∀ Y) (∀ Z) (XεU∧YεV∧X.YεFF∧X.ZεFF⊃Y=Z)⊃(∃ F)
(FεU→V∧(∀ X) (XεU⊃X.β(F,X)εFF)))
AXIOM DIFFSET
(∀ X) (∀ Y) (ISSET X∧ISSET Y⊃ISSET (X-Y)∧(∀ Z) (ZεX-Y≡ZεX∧¬ (ZεY)))
AXIOM BIGUNION
(∀ X) (ISSET X∧(∀ Y) (YεX⊃ISSET Y)⊃ISSET BIGUNION X∧(∀ Z) (Zε
BIGUNION X≡(∃ Y) (YεX∧ZεY)))
AXIOM BIGINTER
(∀ X) (ISSET X∧(∀ Y) (YεX⊃ISSET Y)⊃ISSET BIGINTER X∧(∀ Z) (Zε
BIGUNION X≡(∀ Y) (YεX⊃ZεY)))
AXIOM RELATION
(∀ R) (RELATION R≡ISMAP R∧RANGE R=DOMAIN R→TV)
AXIOM TV
T≠F∧(∀ X) (XεTV≡X=T∨X=F)
AXIOM RRANGE
(∀ F) (ISMAP F⊃(∀ X) (XεRRANGE F≡XεRANGE F∧(∃ Y) (YεDOMAIN F∧β(F,Y)=
X)))
AXIOM EASYREL
(∀ R) (RELATION R⊃(∀ X) (∀ Y) (β(β(R,X),Y)=T≡ββ(X,R,Y)))
AXIOM BETA2
(∀ F) (∀ X) (∀ Y) (β2(F,X,Y)=β(β(F,X),Y))
AXIOM BETA3
(∀ F) (∀ X) (∀ Y) (∀ Z) (β3(F,X,Y,Z)=β(β(β(F,X),Y),Z))
AXIOM BETA4
(∀ F) (∀ X) (∀ Y) (∀ Z) (∀ W) (β4(F,X,Y,Z,W)=β(β(β(β(F,X),Y),Z),W))
AXIOM TRIVIAL
(∀ R) (∀ U) (TRIVIAL(R,U)≡RELATION R∧ISSET U∧U⊂DOMAIN R∧(∀ X) (∀ Y)
(XεU∧YεU⊃ββ(X,R,Y)=F))
AXIOM FINITE1
FINITE NULLSET
AXIOM FINITE2
(∀ U) (∀ X) (ISSET U∧FINITE U⊃FINITE (U∪UNITSET X))
AXIOM INFINITE
(∀ U) (∀ V) (ISSET U∧ISSET V∧INFINITE U∧FINITE V⊃(∃ X) (XεU∧¬ (XεV)
))
AXIOM REFLEX
(∀ X) (X=X)
AXIOM SYMEQ
(∀ X) (∀ Y) (X=Y⊃Y=X)
AXIOM TRANSEQ
(∀ X) (∀ Y) (∀ Z) (X=Y∧Y=Z⊃X=Z)
AXIOM NOTEQ
(∀ X) (∀ Y) (X≠Y≡¬ (X=Y))
AXIOM SI1
SCWORLD W0
AXIOM SI2
I0εBASIS W0
AXIOM SI3
(∀ X) (XεTERMS(TORD I0,W0)⊃SUCC XεTERMS(TORD I0,W0)∧(∀ S) (SεSTATES
W0⊃C(SUCC X,S)=SUCC C(X,S)))
AXIOM SI4
(∀ X) (XεTERMS(TORD I0,W0)⊃PRED XεTERMS(TORD I0,W0)∧(∀ S) (SεSTATES
W0⊃C(PRED X,S)=PRED C(X,S)))
AXIOM SI5
(∀ X) (∀ Y) (XεTERMS(TORD I0,W0)∧YεTERMS(TORD I0,W0)⊃INTEQ(X,Y)ε
TERMS(TORD TV,W0)∧(∀ S) (SεSTATES W0⊃C(INTEQ(X,Y),S)=INTEQ(C(X,S),C
(Y,S))))
SCHEMA COMPREHENSION
(PRED PP) (∀ UU) (ISSET UU⊃(∃ WW) (ISSET WW∧(∀ XX) (XXεWW≡XXεUU∧PP
XX)))
SCHEMA FCOMPREHENSION
(PRED FF) (∀ U) (∀ V) (ISSET U∧ISSET V∧(∀ X) (XεU⊃FF XεV)⊃(∃ F) (FεU
→V∧(∀ X) (XεU⊃β(F,X)=FF X)))
PROOF ONE
1: (∃ X) (∃ Y) (X≠Y∧XεVARS TORD I0∧YεVARS TORD I0) BY ASSUMPTION~
2: (∃ Y) (X≠Y∧XεVARS TORD I0∧YεVARS TORD I0) BY ES(1,X) ASSUMING~
(1)
3: X≠Y∧XεVARS TORD I0∧YεVARS TORD I0 BY ES(2,Y) ASSUMING (1)
4: X≠Y BY AE(3,1) ASSUMING (1)
5: XεVARS TORD I0 BY AE(3,2) ASSUMING (1)
6: YεVARS TORD I0 BY AE(3,3) ASSUMING (1)
7: SUCC2εTERMS(TORD I0→→TORD I0,W0) BY ASSUMPTION
8: PRED2εTERMS(TORD I0→→TORD I0,W0) BY ASSUMPTION
9: (∃ F) (FεVARS (TORD I0→→TORD I0→→TORD I0)) BY ASSUMPTION
10: EQI2εTERMS(TORD I0→→TORD I0→→RTV,W0) BY ASSUMPTION
11: (∀ W) (SCWORLD W⊃(∃ S) (SεSTATES W∧(∀ R) (∀ V) (RεORDERINGS
W∧VεVARS R⊃C(V,S)=UU))) BY ASSUMPTION
12: SCWORLD W0⊃(∃ S) (SεSTATES W0∧(∀ R) (∀ V) (RεORDERINGS W0∧Vε
VARS R⊃C(V,S)=UU)) BY US(11,W0) ASSUMING (11)
13: SCWORLD W0 BY AXIOM SI1
14: (∃ S) (SεSTATES W0∧(∀ R) (∀ V) (RεORDERINGS W0∧VεVARS R⊃C(V
,S)=UU)) BY MP(13,12) ASSUMING (11)
15: SUUεSTATES W0∧(∀ R) (∀ V) (RεORDERINGS W0∧VεVARS R⊃C(V,SUU)=
UU) BY ES(14,SUU) ASSUMING (11)
16: SUUεSTATES W0 BY AE(15,1) ASSUMING (11)
17: (∀ R) (∀ V) (RεORDERINGS W0∧VεVARS R⊃C(V,SUU)=UU) BY AE(15,2
) ASSUMING (11)
18: FPLUSεVARS (TORD I0→→TORD I0→→TORD I0) BY US(9,FPLUS) ASSUMIN~
G (9)
19: SCWORLD W0∧TORD I0εORDERINGS W0∧XεTERMS(TORD I0,W0)∧TORD I0ε
ORDERINGS W0∧SUCC2εTERMS(TORD I0→→TORD I0,W0)∧SεSTATES W0⊃α(SUCC2,X
)εTERMS(TORD I0,W0)∧FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪FREEVARS X∧C
(α(SUCC2,X),S)=β(C(SUCC2,S),C(X,S)) BY AXIOM(SCW12,W0,TORD I0,X,TORD
I0,SUCC2,S)
20: I0εBASIS W0 BY AXIOM SI2
21: SCWORLD W0⊃(∀ U) (UεBASIS W0⊃TORD UεORDERINGS W0) BY AXIOM(
SCW2,W0)
22: (∀ U) (UεBASIS W0⊃TORD UεORDERINGS W0) BY MP(13,21)
23: I0εBASIS W0⊃TORD I0εORDERINGS W0 BY US(22,I0)
24: TORD I0εORDERINGS W0 BY MP(20,23)
25: SCWORLD W0∧TORD I0εORDERINGS W0⊃INFINITE VARS TORD I0∧VARS
TORD I0⊂TERMS(TORD I0,W0) BY AXIOM(SCW7,W0,TORD I0)
26: VARS TORD I0⊂TERMS(TORD I0,W0) BY TAUT(VARS TORD I0⊂TERMS(
TORD I0,W0),25,13,24)
27: VARS TORD I0⊂TERMS(TORD I0,W0)≡(∀ X) (XεVARS TORD I0⊃XεTERMS
(TORD I0,W0)) BY AXIOM(CONTAIN,VARS TORD I0,TERMS(TORD I0,W0))
28: VARS TORD I0⊂TERMS(TORD I0,W0)⊃(∀ X) (XεVARS TORD I0⊃XεTERMS
(TORD I0,W0)) BY EQE(27,1)
29: (∀ X) (XεVARS TORD I0⊃XεTERMS(TORD I0,W0)) BY MP(28,26)
30: XεVARS TORD I0⊃XεTERMS(TORD I0,W0) BY US(29,X)
31: XεTERMS(TORD I0,W0) BY MP(30,5) ASSUMING (1)
32: SεSTATES W0 BY ASSUMPTION
33: SCWORLD W0∧TORD I0εORDERINGS W0∧XεTERMS(TORD I0,W0)∧TORD I0ε
ORDERINGS W0∧SUCC2εTERMS(TORD I0→→TORD I0,W0)∧SεSTATES W0 BY AI(13,
24,31,24,7,32) ASSUMING (1 7 32)
34: α(SUCC2,X)εTERMS(TORD I0,W0)∧FREEVARS α(SUCC2,X)=FREEVARS
SUCC2∪FREEVARS X∧C(α(SUCC2,X),S)=β(C(SUCC2,S),C(X,S)) BY MP(33,19) AS~
SUMING (32 7 1)
35: α(SUCC2,X)εTERMS(TORD I0,W0) BY AE(34,1) ASSUMING (32 7 1)
36: FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪FREEVARS X BY AE(34,2) ASS~
UMING (32 7 1)
37: C(α(SUCC2,X),S)=β(C(SUCC2,S),C(X,S)) BY AE(34,3) ASSUMING (32~
7 1)
38: SεSTATES W0⊃C(α(SUCC2,X),S)=β(C(SUCC2,S),C(X,S)) BY DED(37,
32) ASSUMING (7 1)
39: (∀ S) (SεSTATES W0⊃C(α(SUCC2,X),S)=β(C(SUCC2,S),C(X,S))) BY
UG(38,S) ASSUMING (7 1)
40: SεSTATES W0⊃FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪FREEVARS X BY
DED(36,32) ASSUMING (7 1)
41: (∀ S) (SεSTATES W0⊃FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪
FREEVARS X) BY UG(40,S) ASSUMING (7 1)
42: SUUεSTATES W0⊃FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪FREEVARS X
BY US(41,SUU) ASSUMING (7 1)
43: FREEVARS α(SUCC2,X)=FREEVARS SUCC2∪FREEVARS X BY MP(42,16) AS~
SUMING (1 7 11)
44: SεSTATES W0⊃α(SUCC2,X)εTERMS(TORD I0,W0) BY DED(35,32) ASSUMI~
NG (7 1)
45: (∀ S) (SεSTATES W0⊃α(SUCC2,X)εTERMS(TORD I0,W0)) BY UG(44,S
) ASSUMING (7 1)
46: SUUεSTATES W0⊃α(SUCC2,X)εTERMS(TORD I0,W0) BY US(45,SUU) ASSU~
MING (7 1)
47: α(SUCC2,X)εTERMS(TORD I0,W0) BY MP(46,16) ASSUMING (1 7 11)
48: FREEVARS SUCC2=NULLSET BY ASSUMPTION
49: SCWORLD W0∧TORD I0εORDERINGS W0∧XεVARS TORD I0⊃FREEVARS X=
UNITSET X BY AXIOM(SCW10,W0,TORD I0,X)
50: FREEVARS X=UNITSET X BY TAUT(FREEVARS X=UNITSET X,49,13,24,5
) ASSUMING (1)
51: ZεNULLSET∪UNITSET X≡ZεNULLSET∨ZεUNITSET X BY AXIOM(UNIONAX,
NULLSET,UNITSET X,Z)
52: ¬ (ZεNULLSET) BY AXIOM(NULL1,Z)
53: ZεNULLSET∪UNITSET X≡ZεUNITSET X BY TAUT(ZεNULLSET∪UNITSET X≡
ZεUNITSET X,52,51)
54: ISSET (NULLSET∪UNITSET X)∧ISSET UNITSET X⊃(∀ X1) (X1εNULLSET
∪UNITSET X≡X1εUNITSET X)⊃NULLSET∪UNITSET X=UNITSET X BY AXIOM(
EXTENSIONALITY,NULLSET∪UNITSET X,UNITSET X)
55: ISSET NULLSET BY AXIOM NULLSET
56: XεUNITSET X≡X=X BY AXIOM(UNITSET,X,X)
57: X=X BY AXIOM(REFLEX,X)
58: XεUNITSET X BY TAUT(XεUNITSET X,57,56)
59: XεUNITSET X⊃ISSET UNITSET X BY AXIOM(ISSET,X,UNITSET X)
60: ISSET UNITSET X BY MP(58,59)
61: ISSET NULLSET∧ISSET UNITSET X⊃ISSET (NULLSET∪UNITSET X) BY
AXIOM(UNIONSET,NULLSET,UNITSET X)
62: ISSET NULLSET∧ISSET UNITSET X BY AI(55,60)
63: ISSET (NULLSET∪UNITSET X) BY MP(61,62)
64: ISSET (NULLSET∪UNITSET X)∧ISSET UNITSET X BY AI(63,60)
65: (∀ X1) (X1εNULLSET∪UNITSET X≡X1εUNITSET X)⊃NULLSET∪UNITSET X
=UNITSET X BY MP(54,64)
66: (∀ X1) (X1εNULLSET∪UNITSET X≡X1εUNITSET X) BY UG(53,Z.X1)
67: NULLSET∪UNITSET X=UNITSET X BY MP(66,65)
68: FREEVARS SUCC2∪UNITSET X=UNITSET X BY REPR(67,48,1) ASSUMING ~
(48)
69: FREEVARS SUCC2∪FREEVARS X=UNITSET X BY REPR(68,50,1) ASSUMING~
(48 1)
70: FREEVARS α(SUCC2,X)=UNITSET X BY REPL(43,69,1) ASSUMING (11 7~
48 1)